Operating systems are a key building block in the development of computing systems. Over the several decades since personal computing has become widespread operating systems have substantially increased in complexity. The development of a computer operating system that is backward-compatible to a substantial number of computer applications, but still is secure enough to achieve a high level of assurance of tamper resistance is extremely challenging. However, new business models for pay-per-use or pay-as-you-go computing require a high level of assurance of tamper resistance.